Pensieve Header: The uniqueness of R in β calculus.

SetDirectory["C:\\drorbn\\AcademicPensieve\\2012-01"];
<< betaCalculus.m;
βSimplify = FullSimplify;

{
Rp=R[1,2],
Rm=RInv[1,2],
Rp**Rm,
Rp+(Rm // dP[1->3, 2->4]) // dm[1,3,1] // dm[4,2,2]
} // βForm // ColumnForm

{
Rp=W[1]+Sum[(Subscript[ρ, 10i+j])[c[1], c[2]] ar[i,j], {i,2}, {j,2}],
Rm=W[1]+Sum[(Subscript[σ, 10i+j])[c[1], c[2]]  ar[i,j], {i,2}, {j,2}],
t1=Rp**Rm,
t2=Rp+(Rm // dP[1->3, 2->4]) // dm[1,3,1] // dm[4,2,2]
} /. α_[c[1], c[2]] :> α// βForm // ColumnForm

eqns=Join[
βEquations[t1==W[1]],
βEquations[t2==W[1]]
] /. α_[c[1], c[2]] :> α

eqns /. {(Subscript[ρ, 12]) -> ((-1+(E^(c[1])))/(c[1])), (Subscript[σ, 12]) -> ((-1+(E^(-c[1])))/(c[1])), (Subscript[ρ, _]) -> 0, (Subscript[σ, _]) -> 0} // Simplify

Reduce[eqns /. {(Subscript[ρ, 12]) ->ρ, (Subscript[σ, 12]) -> σ, (Subscript[ρ, _]) -> 0, (Subscript[σ, _]) -> 0}, {c[1], c[2]}]

Solve[eqns /. {(Subscript[ρ, 12]) ->1, (Subscript[σ, 12]) -> σ, (Subscript[ρ, _]) -> 0, (Subscript[σ, _]) -> 0}, {σ}]

{
Rp=W[1]+ar[1,2],
Rm=W[1]-(1/(1+c[1]))ar[1,2],
Rp**Rm,
Rp+(Rm // dP[1->3, 2->4]) // dm[1,3,1] // dm[4,2,2]
} // βForm // ColumnForm

{
Rp=W[1]+α ar[1,2],
Rm=W[1] -(α/(1+α c[1])) ar[1,2],
Rp**Rm,
Rp+(Rm // dP[1->3, 2->4]) // dm[1,3,1] // dm[4,2,2]
} // βForm // ColumnForm

False && SolveAlways[eqns, {c[1], c[2]}]